es-rcv-from(es; e; l; L)
== (e':es-E(es). 
== (e'  L)  ((es-isrcv(es; e')) c ((es-lnk(es; e') = l)  (es-sender(es; e') = e))))
== c (e1,e2:es-E(es). l_before(e1; e2; L; es-E(es))  es-locl(es; e1; e2)) 

latex

---

clarification:

es-rcv-from(es; e; l; L)
== (e':es-E(es). 
== (e'  L  es-E(es))
==  ((es-isrcv(es; e')) c ((es-lnk(es; e') = l  IdLnk)  (es-sender(es; e') = e  es-E(es)))))
== c (e1:es-E(es), e2:es-E(es). l_before(e1; e2; L; es-E(es))  es-locl(es; e1; e2)) 

latex

Definitions	P  Q, (x  l), A c B, b, es-isrcv(es; e), P  Q, IdLnk, es-lnk(es; e), s = t, es-sender(es; e), x:A. B(x), P  Q, l_before(x; y; l; T), es-E(es), es-locl(es; e; e')
FDL editor aliases	es-rcv-from